(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun l1 () Int)
(declare-fun l2 () Int)
(declare-fun l3 () Int)
(declare-fun l4 () Int)
(assert (>= l1 0))
(assert (>= l2 0))
(assert (>= l3 0))
(assert (>= l4 0))
(assert (> (+ (absolute a) (absolute b)) 0))
(assert (= (+ (+ (- 0 l1) l2) (* a l3)) 0))
(assert (= (+ (+ l1 (- 0 l2)) (* b l3)) 0))
(assert (= (+ (+ (* c l3) l4) 1) 0))
(check-sat)
